a, b:|g|. (s(b)) 
(s((~(a)) * (b * a)))
clarification:
norm_subset_p(g;s) ==
a:|g|, b:|g|. (s(b)) (s(((~g)(a)) (*g) (b (*g) a))) | 13,42 |
a, b:|g|. (s(b)) (s((~(a)) * (b * a)))
a:|g|, b:|g|. (s(b)) (s(((~g)(a)) (*g) (b (*g) a)))
| Up | |
| Wellformedness Lemmas | |
| Definitions | x:A. B(x) Q |